g:OGrp. e  |g| 

latex

Up	groups 1
Definitions of Statement	Mon, AbMon, OMon, OCMon, OGrp, |g|
Definitions	|g|, t  T, x:A. B(x), x,y. t(x;y), , x f y, OMon, Mon, AbMon, OCMon, OGrp, x(s1,s2), P & Q, P  Q
Lemmas	ocgrp wf, grp leq wf, grp id wf, grp le wf, assert wf, grp car wf, linorder wf, grp leq weakening eq